1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
/*!
A reduction configuration to keep going until a given condition has been reached, delegating otherwise to another configuration
*/
use super::*;

/// A reduction configuration to keep going until a given condition has been reached, delegating otherwise to another configuration
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct ReduceUntil<R, C> {
    /// The underlying reduction configuration
    pub reduce: R,
    /// An additional termination condition for this reduction
    pub until: C,
}

impl<R, C> ReductionConfig for ReduceUntil<R, C>
where
    R: ReductionConfig,
    C: TerminationCondition,
{
    type AsRef = Self;

    #[inline]
    fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error> {
        self.reduce.register_push_subst(subst)
    }

    #[inline]
    fn register_pop_subst(&mut self) -> Result<(), Error> {
        self.reduce.register_pop_subst()
    }

    #[inline]
    fn register_beta(&mut self) -> Result<(), Error> {
        self.reduce.register_beta()
    }

    #[inline]
    fn register_eta(&mut self) -> Result<(), Error> {
        self.reduce.register_eta()
    }

    #[inline]
    fn eta(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.until.terminate(term, ctx) {
            return Err(Error::StopReduction);
        }
        self.reduce.eta(term, ctx)
    }

    #[inline]
    fn sub(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.until.terminate(term, ctx) {
            return Err(Error::StopReduction);
        }
        self.reduce.sub(term, ctx)
    }

    #[inline]
    fn head(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.until.terminate(term, ctx) {
            return Err(Error::StopReduction);
        }
        self.reduce.head(term, ctx)
    }

    #[inline]
    fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool {
        self.reduce.intersects(filter, code, form)
    }

    #[inline]
    fn as_ref_mut(&mut self) -> &mut Self::AsRef {
        self
    }
}

/// A termination condition
pub trait TerminationCondition {
    /// Whether to terminate a given reduction, given a term
    fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool;
}

impl TerminationCondition for TermId {
    #[inline]
    fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool {
        // Note: we stop when equality *or* inequality is certain.
        let result = self.eq_term_in(term, ctx.eq_ctx());
        result.is_some()
    }
}

impl TerminationCondition for Option<TermId> {
    #[inline]
    fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool {
        if let Some(this) = self {
            this.terminate(term, ctx)
        } else {
            false
        }
    }
}